\begin{tabbing}
$\forall$${\it es}$:ES, $a$:Atom1, $i$:Id.
\\[0ex]$i$ $\parallel$ $a$
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ $\forall$${\it e'}$$\leq$$e$.${\it e'}$ receives $\parallel$ $a$ \& (($\uparrow$first(${\it e'}$)) $\Rightarrow$ es\_state\_when(${\it es}$;${\it e'}$):es\_state(${\it es}$;$i$)$\parallel$$a$)
\\[0ex]$\Rightarrow$ ($e$ sends $\parallel$ $a$ \& es\_state\_when(${\it es}$;$e$):es\_state(${\it es}$;loc($e$))$\parallel$$a$))
\-
\end{tabbing}